Termination w.r.t. Q proof of TRS/secret05aprove2.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
div(x, y) → ify(ge(y, s(0)), x, y)
ify(false, x, y) → divByZeroError
ify(true, x, y) → if(ge(x, y), x, y)
if(false, x, y) → 0
if(true, x, y) → s(div(minus(x, y), y))

Q is empty.